import java.util.Arrays;

import net.sf.javabdd.BDD;
import net.sf.javabdd.BDDFactory;


public class QueensBDDLogic {

	// A BDD that represents conjunction over all 
	// rules for all the positions on the queens board. 
	// Plus one rule that restricts only one queen per column.
	private BDD queenBDDRules;
	
	private BDDFactory factoryBDD;
	private int numberOfQueens;
	
	public QueensBDDLogic(BDDFactory factoryBDD, int numberOfQueens) {
		this.factoryBDD = factoryBDD;
		this.numberOfQueens = numberOfQueens;
	}
	
	public void generateQueenBDDRules() {
		// Initialize queen BDD to true, satisfiable.
		queenBDDRules = factoryBDD.one();
		
		for (int row = 0; row < numberOfQueens; row++) {
			for (int column = 0; column < numberOfQueens; column++) {
				generateRulesForEachBoardPosition(column, row);
			}
		}
		
		// Build a Rule: At least one queen in each column
		generateOneQueenRule();
	}

	private void generateOneQueenRule() {
		BDD oneQueenRule = factoryBDD.zero();
		
		for (int column = 0; column < numberOfQueens; column++) {
	        oneQueenRule = factoryBDD.zero();
			for (int row = 0; row< numberOfQueens; row++) {
				oneQueenRule = oneQueenRule.or(getVariable(column, row));
			}  
			
	        queenBDDRules = queenBDDRules.and(oneQueenRule);
		}
	}

	private BDD getVariable(int column, int row) {
		return factoryBDD.ithVar(getVariableNumber(column,row));
	}

	private void generateRulesForEachBoardPosition(int column, int row) {
		// BDD rules expressed as boolean expressions 
		// Rules are applied to rows, columns and diagonals
		BDD rowBDD = factoryBDD.zero();
		BDD columnBDD = factoryBDD.zero();
		BDD uprightDiagonalBDD = factoryBDD.zero();
		BDD downrightDiagonalBDD = factoryBDD.zero();
		
		// Rule: No queen in the the same row
        for (int k=0; k < numberOfQueens; k++)  {
                if (k != column)
                	rowBDD = rowBDD.or(getVariable(k, row));
        }
        
        rowBDD = makeRuleForCurrentVariable(column, row, rowBDD);
        
        
        // Rule: No queen in the same column
        for (int k=0; k < numberOfQueens; k++)  {
                if (k != row)
                	columnBDD = columnBDD.or(getVariable(column, k));
        }

        columnBDD = makeRuleForCurrentVariable(column, row, columnBDD);
        
        
        // Rule: No queen in the same up right diagonal
        for (int k=0; k < numberOfQueens; k++)  {
                int ll = column + k - row;

                if (ll >= 0 && ll < numberOfQueens)  {
                        if (k != row)
                        	uprightDiagonalBDD = uprightDiagonalBDD.or(getVariable(ll, k));
                }
        }

        uprightDiagonalBDD = makeRuleForCurrentVariable(column, row, uprightDiagonalBDD);

        
        // Rule: No queen in the same down right diagonal
        for (int k=0; k < numberOfQueens; k++)  {
                int ll = row + column - k;

                if (ll >= 0 && ll < numberOfQueens)  {
                        if (k != row)
                        	downrightDiagonalBDD = downrightDiagonalBDD.or(getVariable(ll, k));
                }
        }

        downrightDiagonalBDD = makeRuleForCurrentVariable(column, row, downrightDiagonalBDD);
        
        // Combining all BDD rules into one BDD
        queenBDDRules = queenBDDRules.and(rowBDD);
        queenBDDRules = queenBDDRules.and(columnBDD);
        queenBDDRules = queenBDDRules.and(uprightDiagonalBDD);
        queenBDDRules = queenBDDRules.and(downrightDiagonalBDD);
	}

	private BDD makeRuleForCurrentVariable(int column, int row, BDD bddLine) {
		
		// Current variable represents a queen
		// Then there must not exist another queen in same line
		BDD variable = getVariable(column, row);
		return variable.and(bddLine).not();
	}

	public void restrict(int column, int row) {
		//Get the number of the variable that corresponds to the place the queen has been inserted.
		int varNum = getVariableNumber(column, row);
		
		//Make a BDD for this variable in positive form and apply it to the queen BDD.
		BDD variable = factoryBDD.ithVar(varNum);
		
		//The variable is set to true and used as a restriction on the BDD. Thus removed from the queen BDD.
		queenBDDRules = queenBDDRules.restrict(variable);
	}

	public int getVariableNumber(int column, int row) {
		
		// Get a variable number representing the column and row position on the board
		// Starting from the bottom row and the first column to the left and increment to the right.
		return (row * numberOfQueens) + column;
	}

	public boolean[] getTheValidDomains() {
		boolean validDomains[] = new boolean[numberOfQueens * numberOfQueens]; 

		// Check if the queenBDDRules is satisfiable by restricting the current queen BDD
		// with each BDD variable in the boardBDD representation. 
		for (int i = 0; i < validDomains.length; i++) {
			BDD variable = factoryBDD.ithVar(i);

			// Get restricted BDD with variableBDD = true, removed from the queenBDDRules.
			BDD queenBDDRulesRestricted = queenBDDRules.restrict(variable);

			// If it is okay to put a queen on the board where the variableBDD represents
			// Then we keep record it is satisfiable.
			if (!(queenBDDRulesRestricted.isZero())) {
				validDomains[i] = true;
			}
		}
		
		return validDomains;
	}

}
